public class ClauseForm {
	
	/**
	 * finds any = (equivalence), and then gets its left and right operands. Then it uses the
	 * rule: a = b becomes (a - b) & (b - a)
	 * 
	 * @param input
	 * @return
	 */
	public static String first(String input) {

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == '=') {

				int[] right = getRight(input, i + 1);
				int[] left = getLeft(input, i);

				String leftOperand = input.substring(left[0], left[1]);
				String rightOperand = input.substring(right[0], right[1]);

				String replace = "(" + leftOperand + "-" + rightOperand + ")&("
						+ rightOperand + "-" + leftOperand + ")";

				input = replaceWith(left[0], right[1], input, replace);

			}

		}

		return input;
	}

	/**
	 * Gets the right operand of an operator at index, and returns an array of
	 * [start, end] indices of the operand
	 * 
	 * @param input
	 * @param index
	 * @return
	 */
	private static int[] getRight(String input, int index) {

		int closedBracket = 0, openBracket = 0;

		for (int i = index; i < input.length(); i++) {

			if (input.charAt(i) == '(' || input.charAt(i) == '[')
				openBracket++;
			if (input.charAt(i) == ')' || input.charAt(i) == ']')
				closedBracket++;

			if (closedBracket > openBracket) {
				return new int[] { index, i };
			}

		}

		return null;
	}

	/**
	 * Gets the left operand of an operator at index, and returns an array of
	 * [start, end] indices of the operand
	 * 
	 * @param input
	 * @param index
	 * @return
	 */
	private static int[] getLeft(String input, int index) {

		int closedBracket = 0, openBracket = 0;

		for (int i = index; i > -1; i--) {

			if (input.charAt(i) == '(' || input.charAt(i) == '[')
				openBracket++;
			if (input.charAt(i) == ')' || input.charAt(i) == ']')
				closedBracket++;

			if (openBracket > closedBracket) {
				return new int[] { i + 1, index };
			}

		}

		return null;
	}

	// /////////////////////////////////////////

	/**
	 * finds any - (implication), and then gets its left and right operands. Then it uses the
	 * rule: a - b becomes ~a | b
	 */
	private static String second(String input) {

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == '-') {

				int[] right = getRight(input, i + 1);
				int[] left = getLeft(input, i);

				String leftOperand = input.substring(left[0], left[1]);
				String rightOperand = input.substring(right[0], right[1]);

				String replace = "~" + leftOperand + "|" + rightOperand;

				input = replaceWith(left[0], right[1], input, replace);

			}

		}

		return input.replaceAll("~~", "");
	}

	// /////////////////////////////////////////

	/**
	 * 
	 * loops on the string until it finds a NOT ~ , then it pushes this not to
	 * the right negating its operand: ~(operand). This operand could be a term
	 * or a sentence.
	 * 
	 */
	private static String third(String input) {

		boolean negating = false;
		int closedBracket = 0, openBracket = 0;

		for (int i = 0; i < input.length(); i++) {

			if (negating) {

				// ///////// QUANTIFIERS ////////////////////////////

				if (input.charAt(i) == 'V') {
					input = replaceWith(i, i + 1, input, "E");
					i++;
					continue;
				}

				if (input.charAt(i) == 'E') {
					input = replaceWith(i, i + 1, input, "V");
					i++;
					continue;
				}

				// ///////// BRACKETS //////////////////////////////////

				if (input.charAt(i) == '(' || input.charAt(i) == '[')
					openBracket++;
				if (input.charAt(i) == ')' || input.charAt(i) == ']')
					closedBracket++;

				if (openBracket == closedBracket) {
					negating = false;
					continue;
				}

				// ////////////////////////////////////////////////////
				if (input.charAt(i) == '~') {
					input = replaceWith(i, i + 1, input, "!");
					continue;
				}

				if (atom(input.charAt(i)) && input.charAt(i - 1) != '!') {
					input = replaceWith(i, i + 1, input, "~" + input.charAt(i));
					i++;
					continue;
				}

				if (input.charAt(i) == '&') {
					input = replaceWith(i, i + 1, input, "|");
					continue;
				}

				if (input.charAt(i) == '|') {
					input = replaceWith(i, i + 1, input, "&");
					continue;
				}

			} else {

				if (input.charAt(i) == '~' && !atom(input.charAt(i + 1))) {
					input = replaceWith(i, i + 1, input, "!");
					negating = true;
				}
			}

		}

		return input.replaceAll("!", "");
	}

	/**
	 * returns true if a character is an Atomic
	 * 
	 * @param charAt
	 * @return
	 */
	private static boolean atom(char charAt) {
		return charAt == 'P' || charAt == 'Q' || charAt == 'R';
	}

	/**
	 * Given a string, it replaces the substring from start to end with the
	 * string replace.
	 * 
	 * @param start
	 * @param end
	 * @param input
	 * @param replace
	 * @return
	 */
	public static String replaceWith(int start, int end, String input,
			String replace) {

		input = input.substring(0, start) + replace
				+ input.substring(end, input.length());

		return input;
	}

	// ////////////////////////////////////////

	/**
	 * 
	 * For any quantifier it checks if its variable has already been used. If
	 * yes then it replaces it with a new variable, else go on.
	 * 
	 */
	private static String four(String input) { // will break in case of VxVy

		String vars = "";
		char charFactory = 'a';

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == 'V' || input.charAt(i) == 'E') {

				if (vars.indexOf(input.charAt(i + 1)) > -1) {

					char old = input.charAt(i + 1);

					while (vars.indexOf(charFactory) > -1)
						charFactory++;

					char next = charFactory++;
					input = replaceWith(i + 1, i + 2, input, next + "");
					vars += next;
					i += 1;

					int closedBracket = 0, openBracket = 0;

					int j = i;

					while (input.charAt(j) != '[' && input.charAt(j) != '(')
						j++;

					for (; j < input.length(); j++) {

						// ///////// BRACKETS //////////////////////////////////

						if (input.charAt(j) == old) {
							input = replaceWith(j, j + 1, input, next + "");
						}

						if (input.charAt(j) == '(' || input.charAt(j) == '[')
							openBracket++;
						if (input.charAt(j) == ')' || input.charAt(j) == ']')
							closedBracket++;

						if (openBracket == closedBracket) {
							break;
						}
					}

				} else {

					vars += input.charAt(i + 1);
					i++;

				}

			}

		}

		return input;
	}

	// /////////////////////////////////////////

	/**
	 * 
	 * stores all V variables in a string vars, then if it finds a E it removes
	 * it and replaces all the occurrences of its var with f(vars)
	 * 
	 */
	private static String five(String input) {

		String vars = "";
		char constantFactory = 'A';

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == 'V') {

				char old = input.charAt(i + 1);
				vars += old;
				i += 2;
			}
			if (input.charAt(i) == 'E') {

				char remove = input.charAt(i + 1);
				input = replaceWith(i, i + 2, input, "");

				int closedBracket = 0, openBracket = 0;

				int j = i;

				while (input.charAt(j) != '[' && input.charAt(j) != '(')
					j++;

				for (; j < input.length(); j++) {

					// ///////// BRACKETS //////////////////////////////////

					if (input.charAt(j) == remove) {
						if (!vars.isEmpty()) {
							input = replaceWith(j, j + 1, input, "f(" + vars
									+ ")");
						} else
							input = replaceWith(j, j + 1, input,
									constantFactory + "");
						continue;
					}

					if (input.charAt(j) == '(' || input.charAt(j) == '[')
						openBracket++;
					if (input.charAt(j) == ')' || input.charAt(j) == ']')
						closedBracket++;

					if (openBracket == closedBracket) {
						i = -1; // Make a new run, since the lenght of the
								// string has changed
						break;
					}
				}
				if (vars.isEmpty()) {
					constantFactory++;
				}
			}
		}
		return input;
	}

	// //////////////////////////////////////////

	/**
	 * removes all the V quantifiers
	 */
	private static String six(String input) {

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == 'V') {
				input = replaceWith(i, i + 2, input, "");
			}
		}

		return input;
	}

	// ///////////////////////////////////////////

	/**
	 * Find any OR operator, then get its left and right operands. if one of
	 * them contains an AND then convert it using the rules:
	 * 
	 * (a & b) | c becomes (a | c) & (b | c) a | (b & c) becomes (a | b) & (a |
	 * c)
	 */
	private static String seven(String input) {

		while (!finishedCNF(input)) {

			for (int i = 0; i < input.length(); i++) {

				if (input.charAt(i) == '|') {

					int[] left = getLeft(input, i);
					String leftString = input.substring(left[0], left[1]);
					int[] right = getRight(input, i + 1);
					String rightString = input.substring(right[0], right[1]);

					if (highestOperator(leftString, '&') != null) {

						String a = highestOperator(leftString, '&')[0];
						String b = highestOperator(leftString, '&')[1];
						String c = rightString;

						String replace = "(" + a + "|" + c + ")" + "&" + "("
								+ b + "|" + c + ")";
						input = replaceWith(left[0], right[1], input, replace);

						i = 0;

					} else {

						if (highestOperator(rightString, '&') != null) {

							String b = highestOperator(rightString, '&')[0];
							String c = highestOperator(rightString, '&')[1];
							String a = leftString;

							String replace = "(" + a + "|" + b + ")" + "&"
									+ "(" + a + "|" + c + ")";
							input = replaceWith(left[0], right[1], input,
									replace);

							i = 0;

						}

					}

				}

			}
		}

		return input;
	}

	/**
	 * gets the operator op of any sentence (( ) op ( ))
	 * 
	 * @param input
	 * @param operator
	 * @return
	 */
	private static String[] highestOperator(String input, char operator) {

		int closedBracket = 0, openBracket = 0;

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == '(' || input.charAt(i) == '[')
				openBracket++;
			if (input.charAt(i) == ')' || input.charAt(i) == ']')
				closedBracket++;

			if (input.charAt(i) == operator) {

				if (openBracket - closedBracket == 1) {
					int[] left = getLeft(input, i);
					int[] right = getRight(input, i + 1);
					String leftString = input.substring(left[0], left[1]);
					String rightString = input.substring(right[0], right[1]);
					return new String[] { leftString, rightString };
				}

			}
		}

		return null;
	}

	/**
	 * checks if the input is all ANDs of ORs
	 * 
	 * @param input
	 * @return
	 */
	private static boolean finishedCNF(String input) {

		for (int i = 0; i < input.length(); i++) {

			if (input.charAt(i) == '|') {

				int[] left = getLeft(input, i);

				if (input.substring(left[0], left[1]).indexOf("&") > -1)
					return false;

				int[] right = getRight(input, i + 1);

				if (input.substring(right[0], right[1]).indexOf("&") > -1)
					return false;

			}

		}

		return true;
	}

	// //////////////////////////////////////////

	/**
	 * Flattens the string input using regular expressions
	 */
	private static String eight(String input) {

		String cnf = input;

		cnf = cnf.replaceAll("\\]", ")");
		cnf = cnf.replaceAll("\\[", "(");
		// cnf = cnf.replaceAll("\\(+", "(");
		// cnf = cnf.replaceAll("\\)+", ")");

		/*
		 * for (int i = 0; i < input.length(); i++) {
		 * 
		 * if (input.charAt(i) != '[' && input.charAt(i) != ']') { cnf +=
		 * input.charAt(i);
		 * 
		 * if (input.charAt(i) == '(' || input.charAt(i) == ')') {
		 * 
		 * if (i > 0) { if (canotBeRemoved(input.charAt(i - 1))) { cnf +=
		 * input.charAt(i); } }
		 * 
		 * } else {
		 * 
		 * cnf += input.charAt(i);
		 * 
		 * } } }
		 */

		return cnf;
	}

	// //////////////////////////////////////////

	public static void convertToCNF(String input, boolean trace) {

		input = input.replaceAll(" ", "");

		System.out.println("FOL: " + input);
		System.out.println();

		input = first(input);

		if (trace) {
			System.out.println("1st: " + input);
			System.out.println();
		}

		input = second(input);

		if (trace) {
			System.out.println("2nd: " + input);
			System.out.println();
		}

		input = third(input);

		if (trace) {
			System.out.println("3rd: " + input);
			System.out.println();
		}

		input = four(input);

		if (trace) {
			System.out.println("4th: " + input);
			System.out.println();
		}

		input = five(input);

		if (trace) {
			System.out.println("5th: " + input);
			System.out.println();
		}

		input = six(input);

		if (trace) {
			System.out.println("6th: " + input);
			System.out.println();
		}

		input = seven(input);

		if (trace) {
			System.out.println("7th: " + input);
			System.out.println();
		}

		input = eight(input);

		if (trace) {
			System.out.println("8th: " + input);
			System.out.println();
		}

		System.out.println("CNF: " + input);

	}

	// /////////////////////////////////////////////////

	public static void main(String[] args) {

		// String input = "VxEy[P(x,y) & VxEy[Q(x,y) - ~P(x)]]";
		// String input = "Vx[P(x) = (Q(x) & Ey[Q(y) & R(y,x)])]";
		String input = "Vx[P(x) = (Q(x) & Ey[Q(y) & R(y, x)])]";

		convertToCNF(input, true);

	}

}
